| Definitions | top,  T, guard(T), sq_type(T), band(p; q), let x = a in b(x), R-loc(R), R-Feasible{i:l}(R), A c B, reduce(f; k; as), t.1, deq-member(eq; x; L), fpf-dom(eq; x; f), fpf-empty, Rsends-T(x1), Rsends-knd(x1), Reffect-T(x1), Rsends-dt(x1), Rsends-l(x1), Reffect-knd(x1), Reffect?(x1), Rsends?(x1), R-da(R; i), fpf-cap(f; eq; x; z),   x. t(x), IdLnk, Knd, R-interface-compat(A; B), Rnone?(x1), Rplus?(x1),  b, R-interface(A; B), es_realizer{i:l}, True, P Q, ff, tt, if b then t else f fi , ge(i; j), False,  A, A  B, Y, prop{i:l}, t  T, R-icompat(A; B), P   Q,  x:A. B(x), P  Q, x(s), P  Q, Unit,  ,  ,  , Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rpre(loc; ds; a; p; P), Rsends(ds; knd; T; l; dt; g), Reffect(loc; ds; knd; T; x; f), Rsframe(lnk; tag; L), Rframe(loc; T; x; L), Rinit(loc; T; x; v), Rplus(left; right), Rnone,  |
| Lemmas | fpf-cap-single-join, lnk-decl wf, fpf-join wf, ifthenelse wf, fpf-cap-single1, isrcv-implies, id-deq wf, lnk-decl-cap, IdLnk sq, Knd sq, fpf-single-dom, fpf-dom wf, fpf-join-cap-sq, squash wf, subtype rel wf, bool sq, bool cases, assert-eq-lnk, tagof wf, eq lnk wf, fpf-single wf, R-compat wf, Reffect wf, lnk wf, isrcv wf, normal-type wf, normal-ds wf, Rrframe wf, Rbframe wf, Raframe wf, fpf-empty wf, locl wf, p-outcome wf, fpf-single wf3, Rpre wf, Rsframe wf, Rframe wf, ldst wf, top wf, rcv wf, Kind-deq wf, lsrc wf, R-da wf, fpf-cap wf, Rinit wf, Rsends? wf, Rplus wf, false wf, true wf, Rnone wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, unit wf, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, Rnone? wf, R-interface-Rplus2, Id wf, R-compat-da, R-interface-Rplus, Rplus-right wf, Rplus-left wf, R-size-decreases, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, ge wf, nat properties, not wf, bnot wf, assert wf, Rplus-Feasible, bool wf, Rplus? wf, le wf, es realizer wf, R-Feasible wf, R-interface wf, nat plus wf, R-size wf, nat wf |
